basic
fun_thru_1op(A;B;opa;opb;f) == a:A. f(opa(a)) = opb(f(a)) 

latex

---

clarification:

basic
fun_thru_1op(A;B;opa;opb;f) == a:A. f(opa(a)) = opb(f(a))  B 

latex

Up	gen algebra 1
Wellformedness Lemmas	fun thru 1op wf
Definitions	x:A. B(x)